Math 512: Finite Model Theory Ptime = Fixed point axiomatizable

John Baldwin

February 16, 1997

For any vocabulary τ, let τ^{+} denote τ along with a binary relations symbol S and individual constants F, L. For any τ-structure A, A^{+} denotes the natural expansion to τ^{+} of a standard representation of A with universe |A|.

0.1 Theorem. For any τ for any ϕ ∈ F P (τ^{+}). {A : |A| < ω ∧ A ⊧ ϕ} is decidable in polynomial time.

Proof. (Sketch) A full proof is by induction on complexity of formulas. The key point is that to decide [LF P \overline{x}Xϕ(\overline{x}, S)]\overline{a}, knowing by induction that for any \overline{b}, ϕ(\overline{b}, S) can be decided in polynomial time. So step 0 setting S = ∅, check for each \overline{b} ∈ A^{k}. Let S_{1} be the successful candidates and do Step 1 with S = S_{1}. But there are at most |A|^{k} steps before reaching a fixed point so the whole process is in PTIME.

We show the following theorem of Immerman and Vardi (independently 1982).

0.2 Theorem. Let K be a collection of finite structures of similarity type τ. If K is decidable in PTIME then there is a F P (τ^{+})-sentence ϕ such that

K = {B|τ : B a finite model of ϕ}.

By K is decided in PTIME we mean there is a deterministic Turing machine M such that for some k:

1. M has one read only tape which is exactly the elements of a τ-structure A. For each k-ary relation in τ there are k heads which scan this tape. The Turing machine ‘looks up’ whether \overline{a} ∈ R by the truth of E(h_{1}, … h_{k}) in A.

2. Each cell is printed with either 0 or 1.

3. the one work tape starts begins with all 0’s.

4. M halts in acccepting state in time at most |A|^{k} moves iff A ∈ K. (There is a halt state, h, which is only entered if the machine immediately halts and accepts.)

We want to prove each such class is definable in F P (τ^{+}). We take a τ-structure A (taken in standard position on |A| and ordered in the natural way) as the input tape. We will model the work tape on |A|^{k}. For simplicity, we now assume that τ contains a single binary relation E.

Note that < is in the transitive closure of S and the induced lexiocographic order <^{∗} on |A|^{k} is explicitly definable from < so we consider them in our language henceforth.

We will define by simultaneous induction fixed points for the following relations:

1. binary predicates: H_{0}(x, t),H_{1}(x, t)

2. 2k-ary predicates: B_{0}(\overline{x}, \overline{t}),B_{1}(\overline{x}, \overline{t}), and C_{q}(\overline{x}, \overline{t}) (for each state q).

In dealing with fixed point logic below we are tacitly assuming some of the ‘regularity properties’ of a logic referred to in the previous lecture. E.g. the substitution property (see E and F in Model Theoretic Logics, justifies our use of <^{∗}-below.

For the moment, consider the others as relations on the τ^{+}-structure A. Then a typical rule P for M would say: If in state q with E(h_{1}, h_{2}) (h_{i} are the positions of the two heads on the input tape), the work tape is reading 1 then H_{1} should move left, H_{2} should move right and a 0 should be printed on the work tape and go into state q′.

We code this as follows: [H_{0}(x_{1}, t) ∧ H_{1}(x_{2}, t) ∧ C_{q}(\overline{x}, \overline{t}) ∧ B_{1}(\overline{x}, \overline{t})] ∧ [H_{1}(x − 1, t + 1) ∧ H_{2}(x + 1, t + 1) ∧ B_{0}(\overline{x}, \overline{t} + 1) ∧ C_{q′}(\overline{x}, \overline{t} + 1)

Call this formula θ_{P} (x_{1}, x_{2}, \overline{x}, \overline{t}). (Note that we actually need a couple of more quantifiers to replace functions +1 by relations but these are bound). We describe the initial conditions by a formula θ_{i}(\overline{x}, ¯0): (∀\overline{x},)B_{0}(\overline{x}, ¯0) ∧ C_{i}(¯0, ¯0). Thus C_{q}(\overline{x}, \overline{t}) means that at time \overline{t}. the machine is at cell \overline{x} on the work tape and is in state q. Now consider

(LF P x_{1}, x_{2}, \overline{x}, \overline{t}, X)((∀\overline{x},)θ_{i}(\overline{x}, ¯0) ∧ ⋀_{P}(∃x_{1}, x_{2}, \overline{x}, \overline{t})θ_{P} ,

where X is any of our additional predicates.) The simultaneous fixed points of these relations are the required B_{i}, C_{q}, H_{i}.

The formulas are positive so there clearly is a fixed point. But some argument is needed to show they are the correct relations. In particular to be correct means that at each position and time, each cell of the work tape has either 0 or 1 (not both) (i.e. (∀\overline{x}, \overline{t})B_{0}(\overline{x}, \overline{t}) ∨ B_{1}(\overline{x}, \overline{t}) ∧ ¬(B_{0}(\overline{x}, \overline{t}) ∧ B_{1}(\overline{x}, \overline{t})). ) Similarly at most one C_{q} should hold at each postition. This is proved by routine induction using heavily that M is a deterministic machine.

Finally:

A ∈ K iff A^{+} ⊧ (∃\overline{x}, \overline{t})C_{h}(\overline{x}, \overline{t}).